Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix update of proof tree in case of filter changes (fixes #3367) #3368

Merged
merged 14 commits into from
Dec 13, 2023

Conversation

unp1
Copy link
Member

@unp1 unp1 commented Dec 1, 2023

Related Issue

This pull request addresses #3367

Intended Change

Activating a filter works immediately.

The underlying problem is that the GUIProofTreeModel stores the selection and does not update with the selection model in the ProofTreeView.

This PR does not maintain the consistency. The redundant information was seemingly only thought to be used to store the selected node when switching proofs and restoring it when switching back. The method setFilter should for that reason not query the model for the selection but the view to get an up-to-date path.

Previously it got null (despite a node being selected in the view) and did not activate the filter.

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • Refactoring (behaviour should not change or only minimally change)
  • New feature (non-breaking change which adds functionality)
  • Breaking change (fix or feature that would cause existing functionality to change)
  • There are changes to the (Java) code
  • There are changes to the taclet rule base
  • There are changes to the deployment/CI infrastructure (gradle, github, ...)
  • Other:

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
  • I added new test case(s) for new functionality.
  • I have tested the feature as follows: The steps for reproduction of Proof tree filters not applied correctly #3367 do no longer reproduce the error. Playing around with multiple proofs and selecting filters seems to work.
  • I have checked that runtime performance has not deteriorated.

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@unp1 unp1 self-assigned this Dec 1, 2023
@unp1 unp1 added the 🐞 Bug label Dec 1, 2023
@unp1 unp1 linked an issue Dec 1, 2023 that may be closed by this pull request
@unp1 unp1 added the Review Request Waiting for review label Dec 1, 2023
Copy link

codecov bot commented Dec 1, 2023

Codecov Report

All modified and coverable lines are covered by tests ✅

Comparison is base (abbe1f8) 37.98% compared to head (e032871) 37.98%.

Additional details and impacted files
@@            Coverage Diff            @@
##               main    #3368   +/-   ##
=========================================
  Coverage     37.98%   37.98%           
  Complexity    17024    17024           
=========================================
  Files          2059     2059           
  Lines        126029   126029           
  Branches      21282    21282           
=========================================
  Hits          47874    47874           
  Misses        72272    72272           
  Partials       5883     5883           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

@WolframPfeifer
Copy link
Member

Thanks for the fast response! This PR fixes issue #3367. However, while testing the changes, I think I found another problem that is related (at the moment already present on main branch, but not before the merge of #3349):
Changing the checkboxes in the "View" menu (Pretty printing, Unicode, Syntax Highlighting, ...) does not trigger a redraw. After a "manual" redraw (by switching nodes), the settings are applied correctly.

@unp1
Copy link
Member Author

unp1 commented Dec 1, 2023

I fixed the new issue in the other PR (but we can simply cherry-pick that commit if this PR should be used).

Previously the KeY's selection changed events were misused to cause updates of the GUI (but creating other problems) even so no other proof or node had been selected. The committed fix is not yet ideal, but the main window now redraws when pretty printer settings change. A proper solution would use the ChangeListener (or something similar like moving these changes to the Config class).

@unp1
Copy link
Member Author

unp1 commented Dec 2, 2023

I moved the refactoring (and bugfixes) from #3369 to here, but this PR keeps the old non-local filter semantics

see remark at #3367 (comment) instead

Copy link
Member

@WolframPfeifer WolframPfeifer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I tested the GUI for the use cases that I could think of. Everything worked except the following minor bug: The selection highlights of expanded OSS nodes are not painted anymore (this worked in 2.12.0). The nodes are selected and the sequent is updated as expected (a feature implemented by @FliegendeWurst), just the selection highlight is not (it stays at the parent node).

@unp1
Copy link
Member Author

unp1 commented Dec 8, 2023

Thanks. The highlighting is fixed. It fixes also an exception, if a filter like "Hide Closed Subtrees" is activated, while an OSS child node is selected.
The force push was just a rebase on the current main.

Copy link
Member

@WolframPfeifer WolframPfeifer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks! I tried to come up with the common use cases and tested them. Everything seems to work now.

@WolframPfeifer WolframPfeifer added this pull request to the merge queue Dec 13, 2023
Merged via the queue into main with commit a92f04e Dec 13, 2023
14 checks passed
@WolframPfeifer WolframPfeifer deleted the fix3367 branch December 13, 2023 16:30
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
🐞 Bug Review Request Waiting for review
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Proof tree filters not applied correctly
2 participants